FDL - Nuprl Definition : alle-rcv

Nuprl Definition : alle-rcv

0,22

e=rcv(l,tg). P(e) ==

e:E. kind(e) = rcv(l,tg)

P(e)

clarification:

alle-rcv(es;l;tg;e.P(e)) ==

e:es-E(es). es-kind(es; e) = rcv(l,tg)

Knd

P(e)

Definitions x:A. B(x), E, P Q, Knd, kind(e), rcv(l,tg)

FDL editor aliases alle-rcv

Definitions	x:A. B(x), E, P Q, Knd, kind(e), rcv(l,tg)
FDL editor aliases	alle-rcv